<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01//EN">
<html>
<head>
<meta http-equiv="content-type"
      content="text/html ; charset=UTF-8">
<title>Release Notes for Kananaskis-7 version of HOL 4</title>
<style type="text/css">
<!--
  body {color: #333333; background: #FFFFFF;
        margin-left: 1em; margin-right: 1em }
  code, pre {color: #006400; font-weight: bold; font-family: "Andale Mono", "Lucida Console", monospace; }
  div.footer { font-size: small; display: flex; justify-content: space-between; }
-->
</style>

</head>

<body>
<h1>Notes on HOL 4, Kananaskis-7 release</h1>

<p>We are pleased to announce the Kananaskis-7 release of HOL 4.</p>

<h2 id="contents">Contents</h2>
<ul>
  <li> <a href="#new-features">New features</a> </li>
  <li> <a href="#bugs-fixed">Bugs fixed</a> </li>
  <li> <a href="#new-theories">New theories</a> </li>
  <li> <a href="#new-tools">New tools</a> </li>
  <li> <a href="#new-examples">New examples</a> </li>
  <li> <a href="#incompatibilities">Incompatibilities</a> </li>
</ul>

<h2 id="new-features">New features:</h2>

<ul>

<li><p><code>HolSmtLib</code>
supports <a href="http://research.microsoft.com/en-us/um/redmond/projects/z3/">Z3</a>
proof reconstruction also for goals that involve fixed-width words,
based on bit-blasting (cf. <code>blastLib</code>) and other word
decision procedures.<p></li>

<li><p><code>HolSmtLib</code> provides a translation from HOL into
<a href="http://combination.cs.uiowa.edu/smtlib/">SMT-LIB</a>&nbsp;2
format.  (Support for SMT-LIB&nbsp;1.2 has been
discontinued. <b>Incompatibility</b>.)<p></li>

<li><p><code>HolQbfLib</code> supports checking both validity and
invalidity certificates for Squolem 2.02. (Support for Squolem 1.x has
been discontinued. <b>Incompatibility</b>.)</p></li>

<li><p><code>wordsSyntax.mk_word_replicate</code> computes the width
of the resulting word when applied to a numeral and a fixed-width
word. Minor <b>incompatibility</b>.</p></li>

<li><p>The new <code>numLib.MOD_ss</code> simpset fragment simplifies a number of expressions involving natural number modulus (<code>MOD</code>).
For example, <code>(7*x&nbsp;+&nbsp;3)&nbsp;MOD&nbsp;2</code> will automatically simplify to <code>(x&nbsp;+&nbsp;1)&nbsp;MOD&nbsp;2</code>.


<li><p>User pretty-printers now have to be of a different type.
This <b>incompatibility</b> affects the function <code>add_user_printer</code>.
Users have to write their pretty-printers in a monadic style, where pretty-printing components are linked with an infix <code>&gt;&gt;</code> connective.
The advantage of the new system is that it gives pretty-printers access to information about which variables are bound and free, and the ability to change this status when making recursive calls to the built-in printer.
It will also be easier to extend the system with new functionality along the same lines.

<li><p>The system supports syntax for decimal fractions (<em>e.g.</em>, <code>3.021</code>).
This syntax maps to division terms of the form <em>n</em>&nbsp;/&nbsp;10<em><sup>m</sup></em>.
Thus <code>3.012</code> maps to the term <code>3012&nbsp;/&nbsp;1000</code>.
This transformation is reversed by the pretty-printer.
In the core system, this syntax is enabled for the real, rational and <a href="
#complex">complex</a> theories.

</ul>

<h2 id="bugs-fixed">Bugs fixed:</h2>

<ul>

<li><p><code>numSimps.REDUCE_ss</code> no longer diverges on certain
terms.</p></li>

<li><p>There is now LaTeX notation for the operation of cross-product on sets (written <em>A&nbsp;×&nbsp;B</em>), and for the numeric pairing function (written <em>n&nbsp;⊗&nbsp;m</em>).</p></li>

<li><p>The lexer now tokenizes the input <code>``&quot;(*&quot;``</code> correctly.</p>
<p>Also handle occurrences of such strings in <code>Theory.sig</code> files, which can cause them to become invalid SML.</p>
</li>

<li><p>When making definitions with <code>Define</code> (and <code>Hol_defn</code>, and others), one can now use the boolean equivalence syntax (<code><=></code> or <code>⇔</code>), not just <code>=</code>.</p>
</li>

<li><p>The <code>SimpL</code> and <code>SimpR</code> directives for controlling the position of simplification were only working with binary relations, not functions (such as <code>+</code>, say).
Thanks to Ramana Kumar for the report of the bug.

<li><p>Fix type-parsing bug when array suffixes and normal suffixes (such as <code>list</code>) interact.  Now, both <code>:bool[32]&nbsp;list</code> and <code>:bool&nbsp;list[32]</code> parse correctly.

</ul>

<h2 id="new-theories">New theories:</h2>

<ul>
<li><p>The theory of transcendental functions (<code>transcTheory</code>)
has been extended with a treatment of exponentiation where exponents
can be of type <code>:real</code>.  This is implemented by the (infix)
function <code>rpow</code>.  (The existing function <code>pow</code>
requires a natural number as the exponent.)  Thanks to Umair Siddique
for the definition and theorems.


<li id="complex"><p>
A formalisation of the complex numbers (<code>complexTheory</code>) by Yong Guan, Liming Li, Minhua Wu and Zhiping Shi.
The authors referred to the HOL Light theory by John Harrison and the theory in PVS.
It includes treatments of the complex numbers in the real pair form, the polar form and the exponential form, with basic arithmetic results and some other theorems.

<li><p>A theory of relations based on sets of pairs (<code>set_relationTheory</code>).
Most of the theorems are about orders, including Zorn’s lemma, and a lemma stating that “stream-like” partial orders can be extended to “stream-like” linear orders.
Also add a theorem to <code>llist</code> that “stream-like” linear orders can be converted into lazy lists.
Thanks to Scott Owens for this development.

</ul>

<h2 id="new-tools">New tools:</h2>

<ul>
<li>
<p>A few extra tools in <code>wordsLib</code>:
<dl>
     <dt> <code>WORD_SUB_CONV</code> / <code>WORD_SUB_ss</code>
<dd>
<p> These can be used to simplify applications of unary/binary minus, introducing or eliminating subtractions where possible.
These must <em>not</em> be used simulataneously with <code>srw_ss</code>, <code>WORD_ARITH_ss</code> or <code>WORD_ss</code> (as this will likely result in non-termination).
However, can be used to good effect afterwards.
For example:
<pre>
        wordsLib.WORD_SUB_CONV ``a + -1w * b``
          |- a + -1w * b = a - b

        wordsLib.WORD_SUB_CONV ``-(a - b)``
          |- -(a - b) = b - a

        wordsLib.WORD_SUB_CONV ``a + b * 3w : word2``
          |- a + b * 3w = a - b

        wordsLib.WORD_SUB_CONV ``192w * a + b : word8``
          |- 192w * a + b = b - 64w * a
</pre>

<dt><code>WORD_DIV_LSR_CONV</code>
<dd><p>
         Convert division by a power of two into a right shift.  For example:
<pre>
        wordsLib.WORD_DIV_LSR_CONV ``(a:word8) // 8w``
           |- a // 8w = a &gt;&gt;&gt; 3
</pre>

<dt><code>BITS_INTRO_CONV</code> / <code>BITS_INTRO_ss</code>
<dd>
    <p>     These convert <code>DIV</code> and <code>MOD</code> by powers of two into application of BITS.
         For example:
<pre>
        wordsLib.BITS_INTRO_CONV ``(a DIV 4) MOD 8``;
          |- (a DIV 4) MOD 8 = BITS 4 2 a

        wordsLib.BITS_INTRO_CONV ``(a MOD 32) DIV 8``;
          |- a MOD 32 DIV 8 = BITS 4 3 a

        wordsLib.BITS_INTRO_CONV ``a MOD 2 ** 4``;
          |- a MOD 2 ** 4 = BITS 3 0 a

        wordsLib.BITS_INTRO_CONV ``a MOD dimword (:'a)``;
          |- a MOD dimword (:'a) = BITS (dimindex (:'a) - 1) 0 a
</pre>

<dt><code>n2w_INTRO_TAC &lt;<em>int</em>&gt;</code>
<dd><p> Attempts to convert goals of the form <code>``a = b``</code>, <code>``a&nbsp;&lt;&nbsp;b``</code> and <code>``a &lt;= b``</code> into goals of the form <code>``n2w&nbsp;a = n2w&nbsp;b``</code>, <code>``n2w&nbsp;a &lt;+ n2w&nbsp;b``</code> and <code>``n2w&nbsp;a &lt;=+ n2w&nbsp;b``</code>.
The integer argument denotes the required word size.
This enables some bounded problems (over the naturals) to be proved using bit-vector tactics.
For example, the goal:
<pre>
        `((11 &gt;&lt; 8) (imm12:word16) : word12) &lt;&gt; 0w ==>
         ((31 + 2 * w2n ((11 &gt;&lt; 8) imm12 : word12)) MOD 32 =
          w2n (2w * (11 &gt;&lt; 8) imm12 + -1w : word32))`
</pre>
<p>         can be solved with
<pre>
        STRIP_TAC THEN n2w_INTRO_TAC 32 THEN FULL_BBLAST_TAC
</pre>
</dl>



</ul>

<h2 id="new-examples">New examples:</h2>

<ul>
<li> <p> A mechanisation of first-order and nominal unification done in an accumulator-passing style with <q>triangular</q> substitutions.
In <code>examples/unification/triangular</code>.
<li><p> Some basic category theory (up to the Yoneda lemma), including two categories of <q>sets</q>: one using HOL sets (predicates) and one using the axiomatically introduced type from <code>zfsetTheory</code>.
In <code>examples/category</code>.
</ul>

<h2 id="incompatibilities">Incompatibilities:</h2>

<ul>

<li><p><code>Lib.itotal</code> removed; use <code>Lib.total</code>
instead. Note that <code>handle&nbsp;_</code> is harmful:
exception <code>Interrupt</code> should never be handled without being
re-raised.</p></li>

<li><p><code>Lib.gather</code> removed;
use <code>{Lib,List}.filter</code> instead.</p></li>

<li><p>The ugly situation whereby we had fixities called <code>Prefix</code> and <code>TruePrefix</code>, but <code>Prefix</code> really encoded an absence of fixity, has been done away with.
Now the fixity <code>Prefix</code> codes for what used to be <code>TruePrefix</code>, and in relevant situations where a <code>fixity</code> value was required, a <code>fixity&nbsp;option</code> can be provided instead.
In this situation <code>NONE</code> is used to indicate the absence of a fixity.

<p>The function <code>set_fixity</code> takes a <code>fixity</code>, not a <code>fixity&nbsp;option</code>, so its old ability to remove fixities has disappeared.
If you wish to do this, you should use the function <code>remove_rules_for_term</code>.

</ul>

<hr>
<div class="footer">
<p><em><a href="http://hol.sourceforge.net">HOL 4, Kananaskis-7</a></em></p>
<p>(<a href="kananaskis-6.release.html">Release notes for previous version</a>)</p>
</div>

</body> </html>
